/*
 * Auteurs : 	Bourgeois Jean-Louis	( jeanlouis.bourgeois@gmail.com )
 *		Ciabaud Yoann		( y.ciabaud@gmail.com )
 *
 * Date : Le 15-02-2007
 *
 * Dans ce fichier, sont regroupees les primitives necessaires a
 * l'interpretation d'une formule de cardinalite, par application 
 * de la methode DPC, ainsi que que l'algorithme DPC.
 *
 */

#include "dpc.h"
#include "structure.h"
#include "primitives_structure.h"
#include "graphe.h"

#include <stdlib.h>
#include <stdio.h>
#include <math.h>

#ifdef DOT
/* profondeur */
int niveau = 0;
#endif

/**
 * Objectif :  Choisir un litteral dans le cas d'un branchement
 * @param	*F	Notre Formule
 * @return		Le Litteral Choisi
 */
int heuristiqueLitteral( Formule *F ){

#ifdef H1
	/*** Premier litteral disponible ***/
	int i;

	/* pour chaque litteral */
	for(i=1; i<=F->nbLitteraux; i++)
	{
		if( F->litteraux[i].taille!=0 && F->litteraux[i].etat == INCONNU){

			return i;
		}
	}
	
#elif H3

	/*** Maximum d occurences */
	int i, max=-1;
			
	/* Pour toutes les clauses */
	for( i=1; i<=F->nbLitteraux; i++ ){
		/* si la clause n'est pas affectee */
		if(  F->litteraux[i].taille !=0 && F->litteraux[i].etat == INCONNU){
			if( max==-1 || F->litteraux[i].taille > F->litteraux[max].taille)
				max = i;
		}
	}
	return max;


#elif H2

	/*** Clause la plus grande ***/
	Clause *max = NULL;
	Litteral *I;
	int i;

	for( i=1; i<=F->nbClauses; i++ ){
		if(F->clauses[i]->etat == INCONNU)	
			if(max==NULL||F->clauses[i]->taille > max->taille )
				max = F->clauses[i];
	}
	FOREACH( I, max->tete ){
		i = abs(I->variable);

		if( F->litteraux[i].taille!=0 && F->litteraux[i].etat == INCONNU)
			return i;

	}

#elif H4

	/*** Clause la plus petite ***/
	Clause *min = NULL;
	Litteral *I;
	int i;

	for( i=1; i<=F->nbClauses; i++ ){
		if(F->clauses[i]->etat == INCONNU)	
			if(min==NULL||F->clauses[i]->taille < min->taille )
				min = F->clauses[i];
	}
	FOREACH( I, min->tete ){
		i = abs(I->variable);

		if( F->litteraux[i].taille!=0 && F->litteraux[i].etat == INCONNU)
			return i;

	}

#elif H5

	/*** Difference rho et l ***/
	Clause *min = NULL;
	Litteral *I;
	int i;

	for( i=1; i<=F->nbClauses; i++ ){
		if(F->clauses[i]->etat == INCONNU)	
			if(min==NULL||F->clauses[i]->taille - F->clauses[i]->card < min->taille - min->card )
				min = F->clauses[i];
	}
	FOREACH( I, min->tete ){
		i = abs(I->variable);

		if( F->litteraux[i].taille!=0 && F->litteraux[i].etat == INCONNU)
			return i;

	}

#endif
	
	ERREUR( "Aucun choix possible");

	return 0;

}


/**
 * Objectif :  verifier si on fini de travailler sur la formule <i>F</i>
 * @param	*F	Formule considerre
 * @return		VRAI si termine, FAUX sinon.
 */
int i = 0;
int estTermine( Formule *F ){
	
	return (F->taille == 0)?VRAI:FAUX;
}



/**
 * Objectif : remonter dans l'arborescence, en effancant l'affectation
 * 	de la variable <i>variable</i> dans la formule <i>F</i>
 * @param	*F		Formule etudiee
 * @param	variable	Vaiable Liberee
 */
void libereVariable( Formule *F, int variable){

	int valeur = F->litteraux[abs(variable)].etat;
	ListeClause *listeClause = F->litteraux[abs(variable)].litteraux;
	
	//Libere la variable
	F->litteraux[abs(variable)].etat = INCONNU;
	
	//modifie la taille et la cardinalite de chaque clause
	while( listeClause != NULL )
	{
		if( listeClause->affectee == VRAI )
		{
			//On modifie le nombre d'occurence du litteral
			F->litteraux[abs(variable)].taille++;
					
			//libere la variable
			listeClause->affectee = FAUX;
			
			//Si c'est de signe positif
			if( listeClause->signe == 1 )
			{
				if( valeur == VRAI )
				{
					//On augmente la taille et la cardinalites
					listeClause->clause->card++;
					listeClause->clause->taille++;
					//si elle etait consistante
					if( listeClause->clause->card == 1 )
						F->taille++;
				}
				else
				{
					//On augmente la taille
					listeClause->clause->taille++;
				}
			}
			//signe negatif
			else
			{
				if( valeur == FAUX )
				{
					//On augmente la taille et la cardinalites
					listeClause->clause->card++;
					listeClause->clause->taille++;
					//Si elle etait consistante
					if( listeClause->clause->card == 1 )
						F->taille++;
				}
				else
				{
					//On augmente la taille
					listeClause->clause->taille++;
				}
			}
			//On libere la clause
			listeClause->clause->etat = INCONNU;
		}
		
		//On avance
		listeClause = listeClause->suivant;
	}
}






/**
 * Objectif : 	Affecter la valeur <i>valeur</i> au litteral </i>litteral</l>
 *		dans la formule <i>F</i>
 * @param	*F		Formule etudiee
 * @param	*litteral	litteral affecte
 * @param	valeur		nouvelle valeur de l
 * @return	VRAI		on peut affecter un litteral
 *		INCONSISTANT	modele inconsistant
 */
int affecteLitteral( Formule *F, int litteral, int valeur ){
	
	int retour = VRAI;
	ListeClause *listeClause = F->litteraux[litteral].litteraux;
	
	//Affecte la variable
	F->litteraux[litteral].etat = valeur;
	int i,j=0;
	for( i=1; i<=F->nbClauses; i++)
		if( F->clauses[i]->etat == INCONNU )j++;
	
	
	//modifie la taille et la cardinalite de chaque clause
	while( listeClause != NULL )
	{
		if( listeClause->clause->etat == INCONNU )
		{
			//On modifie le nombre d'occurence du litteral
			F->litteraux[abs(litteral)].taille--;
			
			listeClause->affectee = VRAI;

			//Si c'est de signe positif
			if( listeClause->signe == 1 )
			{
				
				if( valeur == VRAI )
				{
					//On diminue la taille et la cardinalites
					listeClause->clause->card--;
					listeClause->clause->taille--;
					//Est elle consistante
					if( listeClause->clause->card == 0 )
					{
						listeClause->clause->etat = CONSISTANT;
						F->taille--;
					}
				}
				else
				{
					//On diminue la taille
					listeClause->clause->taille--;
					//Est elle consistante
					if( listeClause->clause->card >  listeClause->clause->taille)
					{
						listeClause->clause->etat = INCONSISTANT;
						retour = INCONSISTANT;
					}
				}
			}
			//signe negatif
			else
			{
				if( valeur == FAUX )
				{
					//On diminue la taille et la cardinalites
					listeClause->clause->card--;
					listeClause->clause->taille--;
					//Est elle consistante
					if( listeClause->clause->card == 0 )
					{
						listeClause->clause->etat = CONSISTANT;
						F->taille--;
					}
				}
				else
				{
					//On diminue la taille
					listeClause->clause->taille--;
					//Est elle consistante
					if( listeClause->clause->card >  listeClause->clause->taille)
					{
						listeClause->clause->etat = INCONSISTANT;
						retour = INCONSISTANT;
					}
				}
			}
		}
		listeClause = listeClause->suivant;
	}


	
	return retour;
}



/**
 * Objectif : Recherche et affecte la premiere clause mono-litterale rencontree.
 * @param	*F		la formule etudiee
 * @param	*litteral	Litteral
 * @return	VRAI		on peut affecter un mono-litteral
 *		FAUX		aucun mono-litteral
 *		INCONSISTANT	un mono-litteral existe, mais modele inconsistant
 */
int affecteMonoLitteraux( Formule *F, int *litteral ){

	Litteral *l;
	int i;
	
	//pour toutes les clauses
	for( i=1; i<=F->nbClauses; i++)
	{
		//si c'est une monoLitterale
		if( F->clauses[i]->taille != 0 && F->clauses[i]->card ==  F->clauses[i]->taille )
		{
	

			//On recherche la variable
			l = F->clauses[i]->tete;
			while( l != NULL )
			{
				if( F->litteraux[abs(l->variable)].etat == INCONNU )
				{
					*litteral = l->variable;
#ifdef DOT
					/* ajoute un etat au graphe */
					ajouterFils( *F, niveau, MONO, l->variable );
#endif
					
					if( affecteLitteral( F, abs(l->variable), (l->variable>0)?VRAI:FAUX ) == INCONSISTANT )
					{
						libereVariable( F, *litteral);
						return INCONSISTANT;
					}

					return VRAI;
				}
				l = l->suivant;
			}
			
			ERREUR("Mono-Litteral Mysterieux...");

		}
	}

	return FAUX;
}









/**
 * Objectif : Recherche un litteral pur et tente une affectation
 * @param	*F		La formule etudiee
 * @param	*litteral	Litteral affecte
 * @return	VRAI 		si un litteral est trouve et une affectation possible.
 *		FAUX 		si aucun litteral pur n'existe.
 *		INCONSISTANT	si un litteral est trouve mais pas une affectation.
 */
int affecteLitterauxPurs( Formule *F, int *litteral ){
	
	int i;
	int signe;
	ListeClause *listeClause;
	
		
	//pour tout les litteraux
	for( i=1; i<=F->nbLitteraux; i++)
	{
		//si le litteral n' pas ete affecte
		if( F->litteraux[i].taille != 0 && F->litteraux[i].etat == INCONNU )
		{
			//pour toutes les clauses (Inconnues)
			listeClause = F->litteraux[i].litteraux;
			signe = 0;
			while( listeClause != NULL )
			{
				//Si la clause est inconnue
				if( listeClause->clause->etat == INCONNU )
				{
					if( signe == 0 )
						signe = listeClause->signe;
					else if( signe !=  listeClause->signe )
						break;
				}
				listeClause = listeClause->suivant;
			}

			//Si i est un litteral pur
			if( listeClause == NULL && signe != 0 )
			{
				*litteral = i;
				
#ifdef DOT
				/* ajoute un etat au graphe */
				ajouterFils( *F, niveau, PUR, signe*i );
#endif

				if( affecteLitteral( F, i, (signe==1)?VRAI:FAUX ) == INCONSISTANT )
				{
					libereVariable( F, *litteral);
					return INCONSISTANT;
				}
				
				return VRAI;


			}
		}
	}
	


	return FAUX;
}



/**
 * Objectif : tester si la formule <i>F<i/> est consistante
 *	<i>dpcRecursif</i>
 * @param	*F		Formule a tester
 * @return	CONSISTANT	si la formule est satisfiable
 *		INCONSISTANT	sinon
 */
int dpc( Formule *F ){

#ifdef DOT
	int i;
#endif
	
	//litteral affecte
	int litteral;
	//Si toute les variable on ete affectee c'est termine
	if( estTermine( F ) == VRAI ){
#ifdef COUNT
	nbSolutions++;
#endif
		return CONSISTANT;
	}
	
	
	//On cherche une clause ML
	int retour = affecteMonoLitteraux( F, &litteral );

	//Si on la trouve
	if(  retour == VRAI ){

#ifdef DOT
		niveau++;
#endif

		if( dpc( F ) == INCONSISTANT ){
			
			libereVariable( F, litteral );
			return INCONSISTANT;
		}
		else{
			libereVariable( F, litteral);
			return CONSISTANT;
		}
	}
	//Si on en trouve pas
	else if( retour == FAUX ){
		
		retour = affecteLitterauxPurs( F , &litteral);

		//Si on trouve un litteral pur
		if( retour == VRAI ){

#ifdef DOT
			niveau++;
#endif

			if( dpc( F ) == INCONSISTANT ){
			
				libereVariable( F, litteral);
				return INCONSISTANT;
			}
			else{
				libereVariable( F, litteral);
				return CONSISTANT;
			}
		}
		//Si on en trouve pas on branche
		else if( retour == FAUX ){
			
			//Choisi un Litteral
			int litteral = heuristiqueLitteral( F );
		
			
	
#ifdef DOT
			/* ajoute un etat au graphe */
			i = niveau;
			ajouterFils( *F, niveau++, CHOIX, litteral );
#endif

			//On lui affecte la premiere valeur
			//Si on peut peut lui affecter on descend
			if( affecteLitteral( F, abs(litteral), (litteral>0)?VRAI:FAUX ) != INCONSISTANT ){
			
				//Si le modele est consistant c'est gagne
				if( dpc( F ) == CONSISTANT ){
#ifndef COUNT
					return CONSISTANT;
#endif
				}
			}
			
			//On se remet dans l'etat
			libereVariable( F, abs(litteral));
			
#ifdef DOT
			/* ajoute un etat au graphe */
			niveau = i;
			ajouterFils( *F, niveau++, CHOIX, -1*litteral );
#endif
			
			//On lui affecte la premiere valeur
			//Si on peut peut lui affecter on descend
			if( affecteLitteral( F, abs(litteral), (litteral>0)?FAUX:VRAI ) != INCONSISTANT ){
			
				//Si le modele est consistant c'est gagne
				if( dpc( F ) == CONSISTANT ){
					libereVariable( F, litteral);
					return CONSISTANT;
				}
			}
			
			//On se remet dans l'etat
			libereVariable( F, abs(litteral));
			
			//On remonte
			return INCONSISTANT;
		}
		//sinon c'est inconsistant
		else {
			
			return INCONSISTANT;
		}

	}
	//Sinon c'est inconsistant
	else {
		
		return INCONSISTANT; 
	}
	
}





/**
 * Objectif : tester si la formule <i>F<i/> est consistante
 *	<i>dpcIteratif</i>
 * @param	*F		Formule a tester
 * @return	CONSISTANT	si la formule est satisfiable
 *		INCONSISTANT	sinon
 */
int dpcIteratif( Formule *F ){

	Historique *historique = NULL;
	Historique *chainon, *tmp;
	int litteral;
	int retour;
	int remonte = 0;

	//tant que ce n'est pas consistant
	while( estTermine( F ) == FAUX ){

		//On cherche une clause ML
		retour = affecteMonoLitteraux( F, &litteral );
		//Si on la trouve
		if(  retour == VRAI ){
			
#ifdef DOT
			niveau++;
#endif
			//On l'ajoute a l'historique
			chainon = calloc(1, sizeof(Historique));
			chainon->variable = litteral;
			chainon->branchement = NON;
			chainon->suivant = historique;
			historique = chainon;
		}
		//Si on en trouve pas
		else if( retour == FAUX ){

			retour = affecteLitterauxPurs( F , &litteral);

			//Si on trouve un litteral pur
			if( retour == VRAI ){
#ifdef DOT
				niveau++;
#endif
				//On l'ajoute a l'historique
				chainon = calloc(1, sizeof(Historique));
				chainon->variable = litteral;
				chainon->branchement = NON;
				chainon->suivant = historique;
				historique = chainon;
			}
			//Si on en trouve pas on branche
			else if( retour == FAUX ){
			
				//Choisi un Litteral
				litteral = heuristiqueLitteral( F );
		
				//Si aucun litteral n'est disponible[CAs improbable!)]
				if( litteral == 0)return INCONSISTANT;
				
#ifdef DOT
				ajouterFils( *F, niveau++, CHOIX, litteral );
#endif
				
				chainon = calloc(1, sizeof(Historique));
				chainon->variable = litteral;
				chainon->branchement = PREMIER;
				chainon->suivant = historique;
				historique = chainon;
				
				//On lui affecte la premiere valeur
				//Si on peut peut lui affecter on descend
				if( affecteLitteral( F, abs(litteral), (litteral>0)?VRAI:FAUX ) == INCONSISTANT )
					remonte = 1;
				
			}
			//sinon c'est inconsistant
			else {
				remonte = 1;
			}

		}
		//Sinon c'est inconsistant
		else {
			remonte = 1;
		}
#ifdef COUNT
	if( estTermine(F) == VRAI ){
		nbSolutions++;
		remonte = 1;
	}
#endif
		//Si on doit remonter
		if( remonte == 1 ){
			
			while( historique!=NULL ){
				
				tmp = historique;
				libereVariable(F, abs(tmp->variable));
#ifdef DOT 
				niveau--;
#endif
				if(  historique->branchement == PREMIER )
				{
					historique->branchement = SECOND;
#ifdef DOT
					ajouterFils( *F, niveau++, CHOIX, -1*historique->variable );
#endif
					if( affecteLitteral( F, abs(historique->variable), (historique->variable>0)?FAUX:VRAI ) != INCONSISTANT )
						break;
				}

				historique = historique->suivant;
				free(tmp);
			}
			
			if(historique == NULL)
				return INCONSISTANT;
			
			remonte = 0;
		}
		
	}
	while( historique != NULL ){
		
		tmp = historique;
		historique = historique->suivant;
		free(tmp);
	}


#ifdef DOT
	Consistant(niveau);
#endif

	return CONSISTANT;
	
}

